The present invention relates generally to verification of cache coherency in a computer system, and more specifically, to cache coherency verification using ordered lists.
Operations in a cache of a computer system may be modeled, and the model compared to the actual state of the cache, in order to determine coherency of the cache. Cache coherency in out-of-order, virtual multi-threaded, multi-core, or multiprocessor computer systems can be relatively complex to model, as the coherency specifications for such devices may have strict rules regarding how each component in the device observes and updates data, but may not dictate how those operations are actually achieved. The goal of the coherency model is to enforce the coherency rules. Micro-architectures may make use of the flexibility of the coherency rules, and even appear to violate the coherency rules in the short term, in order to increase performance. The coherency modeling system will dictate the granularity of the coherency modeling, the design variance and amount of change that can be tolerated, the types of errors that can be caught by the coherency modeling system, and overall ease of debugging.
Some coherency modeling systems utilize one or more timestamps for each cache line access, and a system to update and compare those timestamps to prevent violation of the coherency rules. Use of timestamps requires a very thorough understanding of the access times of the microarchitecture, and may not be very resilient to any changes that affect that timing. Other coherency modeling systems comprise finite state machines, in which coherency events transition the model from one legal state to another, either as a state by state simulation, or as a formal state space exploration of the implemented logic. These approaches are often high-level and may require generalizations for each state, and may preclude some lower level checking of the implementation that may be beneficial during the design phase. Further coherency modeling systems create a graph of all cache accesses and ensure that the vertices followed from the beginning of execution to the end are all legal.